Issue1005.agda:8,19-20
x₁ != x of type X
when checking that the expression t has type T x
